Notes sur la sémantique des langages de programmation

La sémantique (le sens) d'un langages de programmation est définie en termes de la sémantique de ces constructions nonterminaux. Par exemple, le sens d'une définition de constante (dans un programme) est la valeur de la constante, le sens de la définition d'un type de données est normalement l'ensemble des valeurs possibles qui appartiennent au type, le sens d'une expression est la valeur de l'expression et le sens d'un énoncé est l'effet que l'exécution de cet énoncé a sur les valeurs de variables stockées en mémoire.

Certaines propriétés sémantique peuvent être évaluées lors de la compilation; elles sont appelées la "sémantique statique". Par exemple, dans un langage avec typage, le type de la valeur d'une expression peut être évalué par le compilateur, mais la valeur de l'expression dépend normalement de valeurs de variables qui sont connues seulement pendant la phase d'exécution.

La sémantique statique est souvent représentée par des attributs sémantiques qui sont associés aux nonterminaux. (Les attributs seront évalués par le compilateur et seront associés aux noeuds nonterminaux de l'arbre syntaxique qui a été construit par le compilateur). Par exemple, chaque noeud <expression> dans l'arbre syntaxique pourrait avoir un attribut, appelé "type", qui contient comme valeur le type de l'expression. Pour plus de détails, voir le livre de Sebesta, section 3.5.

Il existent différentes méthodes pour la définition de la sémantique dynamique des langages de programmation. Ces méthodes peuvent être classifiées dans les catégories suivantes:

• Définition informelle: Seulement des explications informelles sont données (en langue courante) sur le sens des programmes que l'on peut construire dans le langages (e.g. manuel de référence du langages, etc.)
• Sémantique opérationnelle: Le sens d'une construction dans le langage de programmation est donné en terme de sa traduction dans une autre langage du plus bas niveau, et de la sémantique de ce langage. Normalement, seulement la traduction est définie formellement, la sémantique du langage de bas niveau est définie informellement.
• Sémantique dénotationnelle: Le sens d'un énoncé est défini dans la forme d'une fonction (mathématique) qui a comme argument l'état des variables avant l'exécution de l'énoncé, et qui a comme résultat l'état des variables après l'exécution de l'énoncé. Par exemple, pour un énoncé d'affectation, la fonction est l'identité excepté que la valeur de la variable qui est affectée sera changée à la valeur de l'expression. Il est à noter que le sens d'une expression est une fonction qui a comme argument l'état des variables en mémoire et qui a comme résultat la valeur de l'expression (évaluée dans le contexte de l'état actuel des variables; elle pourrait en dépendre). La fonction qui représente la sémantique d'une boucle est définie récursivement en appliquant la fonction correspondant au corps de la boucle un nombre indéterminé de fois.
• Sémantique axiomatique: Le sens d'un énoncé est donné en fournissant des axiomes sur les propriétés de la fonction qui représentera la sémantique (comme dans la cas de la sémantique dénotationnelle). Cet approche est similaire à l'approche qui est utilisé pour définir la sémantique d'une procédure (indépendamment du code de son corps) par des pré- et post-conditions qui définissent des propriétés pour les paramètres d'entrée et de sortie et l'état des variables. Dans ce contexte, Dijkstra a introduit la notion de la pré-condition la plus faible: pour un énoncé donné et une post-condition donnée qui devrait être valide après l'exécution de l'énoncé en question, la pré-condition la plus faible est la condition la plus faible qui assure, si elle est satisfait juste avant l'exécution de l'énoncé, que la post-condition soit satisfait après l'exécution de l'énoncé.

Un exemple: Définitions de la sémantique des expressions régulières

• Définition informelle: voir première page de la polycopie de "Using Lex".
• Définition informelle, mais déjà beaucoup plus formalisé: définition donné dans mes notes de cours:
  • Les expressions régulières représentent une manière simple pour définir de langages formels à partir des symboles de l'alphabet, la chaîne vide є et les opérateurs de langages suivants: concatenation, union et opérateur de Kleene. Il existent différents notations pour l'union ( "+" ou  "׀"  ) et les opérateurs peuvent avoir différentes priorités. En général, l'opérateur de Kleene a la plus grande priorité.
    • "є" est une expression régulière qui représente le langage {є}
    • si a est un symbole de l'alphabet, alors "a"  est une expression régulière qui représente le langage {a}
    • si une expression "<e>" représente le langage L, alors "<e>*" représente L*
    • si les expressions régulières "<e1>" et "<e1>" représentent les langages L1 et L2, respectivement, alors "<e1>  <e2>" représente L1 . L2
    • si les expressions régulières "<e1>" et "<e1>"  représentent les langages L1 et L2, respectivement, alors "<e1> + <e2>" représente L1 U L2
    • si "<e>" est une expression régulière, alors "(<e>)" est aussi une expression régulière qui représente le même langage
• Définition formelle de type dénotationnelle: Utilisant la grammaire pour les expressions régulières donnée plus haut et adoptant la notation des attributs sémantiques du livre de Sebesta, nous pouvons donner la définition suivante.
  •  Déclaration des attributs sémantiques: le non-terminal RegExpr a un attribut nommé S (pour "sémantique") de type "ensemble de chaînes de terminaux".

  • Grammaire et règles d'évaluation des attributs:

    RegExp[1] -->   (  RegExpr[2]  )

        régle sémantique: RegExp[1].S <-- RegExp[2].S

    RegExpr  --> a 

        régle sémantique: RegExp.S <-- {a}  (et similairement pour b et c)

    RegExpr  -->   ε

        régle sémantique: RegExp.S <-- {ε}

    RegExpr[1] --> RegExpr[2]  RegExpr  [3]

        régle sémantique: RegExp[1].S <-- RegExp[2].S concatenate  RegExp[3].S

    RegExpr[1] --> RegExpr[2]  +  RegExpr  [3]

        régle sémantique: RegExp[1].S <-- RegExp[2].S  union  RegExp[3].S

    RegExpr[1] --> RegExpr[2]  *

        régle sémantique: RegExp[1].S <-- fermeture de Kleene de (RegExp[2].S)